package sketch.specs.symbc;

import gov.nasa.jpf.symbc.Debug;

public class MyClassDouble {
	
	public void myMethod(double x, double y) {
		if(x > 0.8) {
			if(y < 4000.9) {
				System.out.println("reach here x y is true");
			} else {
				System.out.println("reach here x true y is false");
			}
		} else {
			if(x + y > 3.2) {
				System.out.println("reach here x false y is true");
			} else if (x - y < 0.99) {
				System.out.println("reach here x false y is false");
			}
		}
	}
	
	// The test driver
	public static void main(String[] args) {
		MyClassDouble mc = new MyClassDouble();
		mc.myMethod(0.0d, 0.0d);
		Debug.printPC("\nMyClassDouble.myMethod Path Condition: ");
	}
	
}
